T,A:Type, f,g:(TAT), L:(A List), y,z:T.
(L':(A List), a:A.
iseg(A; append(L'; cons(a; [])); L)
 (f(list_accum(x,a.f(x,a); y; L'),a) = g(list_accum(x,a.f(x,a); y; L'),a)))
 (y = z)
 (list_accum(x,a.f(x,a); y; L) = list_accum(x,a.g(x,a); z; L)  T) 

latex

Definitions	t  T, x(s1,s2), x,y. t(x;y), x:A. B(x), list_accum(x,a.f(x;a); y; l), prop{i:l}, P  Q, append(as; bs), iseg(T; l1; l2), guard(T), x. t(x), top, subtype(S; T)
Lemmas	iseg weakening, iseg append, list accum append, top wf, last induction, iseg wf, append wf, list accum wf